Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		f(x,nil)	→ g(nil,x)
2:		f(x,g(y,z))	→ g(f(x,y),z)
3:		x ++ nil	→ x
4:		x ++ g(y,z)	→ g(x ++ y,z)
5:		null(nil)	→ true
6:		null(g(x,y))	→ false
7:		mem(nil,y)	→ false
8:		mem(g(x,y),z)	→ or(y = z,mem(x,z))
9:		mem(x,max(x))	→ not(null(x))
10:		max(g(g(nil,x),y))	→ max'(x,y)
11:		max(g(g(g(x,y),z),u))	→ max'(max(g(g(x,y),z)),u)

There are 5 dependency pairs:


12:		F(x,g(y,z))	→ F(x,y)
13:		x ++# g(y,z)	→ x ++# y
14:		MEM(g(x,y),z)	→ MEM(x,z)
15:		MEM(x,max(x))	→ NULL(x)
16:		MAX(g(g(g(x,y),z),u))	→ MAX(g(g(x,y),z))

The approximated dependency graph contains 4 SCCs: {13}, {12}, {16} and {14}.

Consider the SCC {13}. There are no usable rules. By taking the AF π with π(++#) = 2 and π(g) = [1] together with the lexicographic path order with empty precedence, rule 13 is strictly decreasing.

Consider the SCC {12}. There are no usable rules. By taking the AF π with π(F) = 2 and π(g) = [1] together with the lexicographic path order with empty precedence, rule 12 is strictly decreasing.

Consider the SCC {16}. There are no usable rules. By taking the AF π with π(MAX) = 1 and π(g) = [1] together with the lexicographic path order with empty precedence, rule 16 is strictly decreasing.

Consider the SCC {14}. There are no usable rules. By taking the AF π with π(MEM) = 1 and π(g) = [1] together with the lexicographic path order with empty precedence, rule 14 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.01 seconds) --- May 4, 2006